The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

S is empty.
Rewrite Strategy: INNERMOST

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
rev_l#2/1
Cons/0
step_x_f#1/1
step_x_f/1

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

rev_l#2(x8) → Cons(x8)
step_x_f#1(rev_l, step_x_f(x2, x4), x1) → step_x_f#1(x2, x4, rev_l#2(x1))
step_x_f#1(rev_l, fleft_op_e_xs_1, x3) → rev_l#2(x3)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x6)) → step_x_f(rev_l, foldr#3(x6))
main(Nil) → Nil
main(Cons(x9)) → step_x_f#1(rev_l, foldr#3(x9), Nil)

S is empty.
Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8) → Cons(x8)
step_x_f#1(rev_l, step_x_f(x2, x4), x1) → step_x_f#1(x2, x4, rev_l#2(x1))
step_x_f#1(rev_l, fleft_op_e_xs_1, x3) → rev_l#2(x3)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x6)) → step_x_f(rev_l, foldr#3(x6))
main(Nil) → Nil
main(Cons(x9)) → step_x_f#1(rev_l, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_rev_l2_0 :: rev_l
hole_step_x_f:fleft_op_e_xs_13_0 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_15_0 :: Nat → step_x_f:fleft_op_e_xs_1

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
step_x_f#1, foldr#3

(8) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8) → Cons(x8)
step_x_f#1(rev_l, step_x_f(x2, x4), x1) → step_x_f#1(x2, x4, rev_l#2(x1))
step_x_f#1(rev_l, fleft_op_e_xs_1, x3) → rev_l#2(x3)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x6)) → step_x_f(rev_l, foldr#3(x6))
main(Nil) → Nil
main(Cons(x9)) → step_x_f#1(rev_l, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_rev_l2_0 :: rev_l
hole_step_x_f:fleft_op_e_xs_13_0 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_15_0 :: Nat → step_x_f:fleft_op_e_xs_1

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(gen_Cons:Nil4_0(x))
gen_step_x_f:fleft_op_e_xs_15_0(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_15_0(+(x, 1)) ⇔ step_x_f(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(x))

The following defined symbols remain to be analysed:
step_x_f#1, foldr#3

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(+(1, n7_0), b)), rt ∈ Ω(1 + n7₀)

Induction Base:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(0), gen_Cons:Nil4_0(b)) →_R^Ω(1)
rev_l#2(gen_Cons:Nil4_0(b)) →_R^Ω(1)
Cons(gen_Cons:Nil4_0(b))

Induction Step:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(+(n7_0, 1)), gen_Cons:Nil4_0(b)) →_R^Ω(1)
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), rev_l#2(gen_Cons:Nil4_0(b))) →_R^Ω(1)
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), Cons(gen_Cons:Nil4_0(b))) →_IH
gen_Cons:Nil4_0(+(+(1, +(b, 1)), c8_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(10) Complex Obligation (BEST)

(11) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8) → Cons(x8)
step_x_f#1(rev_l, step_x_f(x2, x4), x1) → step_x_f#1(x2, x4, rev_l#2(x1))
step_x_f#1(rev_l, fleft_op_e_xs_1, x3) → rev_l#2(x3)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x6)) → step_x_f(rev_l, foldr#3(x6))
main(Nil) → Nil
main(Cons(x9)) → step_x_f#1(rev_l, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_rev_l2_0 :: rev_l
hole_step_x_f:fleft_op_e_xs_13_0 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_15_0 :: Nat → step_x_f:fleft_op_e_xs_1

Lemmas:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(+(1, n7_0), b)), rt ∈ Ω(1 + n7₀)

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(gen_Cons:Nil4_0(x))
gen_step_x_f:fleft_op_e_xs_15_0(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_15_0(+(x, 1)) ⇔ step_x_f(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(x))

The following defined symbols remain to be analysed:
foldr#3

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldr#3(gen_Cons:Nil4_0(n499_0)) → gen_step_x_f:fleft_op_e_xs_15_0(n499_0), rt ∈ Ω(1 + n499₀)

Induction Base:
foldr#3(gen_Cons:Nil4_0(0)) →_R^Ω(1)
fleft_op_e_xs_1

Induction Step:
foldr#3(gen_Cons:Nil4_0(+(n499_0, 1))) →_R^Ω(1)
step_x_f(rev_l, foldr#3(gen_Cons:Nil4_0(n499_0))) →_IH
step_x_f(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(c500_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(13) Complex Obligation (BEST)

(14) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8) → Cons(x8)
step_x_f#1(rev_l, step_x_f(x2, x4), x1) → step_x_f#1(x2, x4, rev_l#2(x1))
step_x_f#1(rev_l, fleft_op_e_xs_1, x3) → rev_l#2(x3)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x6)) → step_x_f(rev_l, foldr#3(x6))
main(Nil) → Nil
main(Cons(x9)) → step_x_f#1(rev_l, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_rev_l2_0 :: rev_l
hole_step_x_f:fleft_op_e_xs_13_0 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_15_0 :: Nat → step_x_f:fleft_op_e_xs_1

Lemmas:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(+(1, n7_0), b)), rt ∈ Ω(1 + n7₀)
foldr#3(gen_Cons:Nil4_0(n499_0)) → gen_step_x_f:fleft_op_e_xs_15_0(n499_0), rt ∈ Ω(1 + n499₀)

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(gen_Cons:Nil4_0(x))
gen_step_x_f:fleft_op_e_xs_15_0(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_15_0(+(x, 1)) ⇔ step_x_f(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(x))

No more defined symbols left to analyse.

(15) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(+(1, n7_0), b)), rt ∈ Ω(1 + n7₀)

(16) BOUNDS(n^1, INF)

(17) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8) → Cons(x8)
step_x_f#1(rev_l, step_x_f(x2, x4), x1) → step_x_f#1(x2, x4, rev_l#2(x1))
step_x_f#1(rev_l, fleft_op_e_xs_1, x3) → rev_l#2(x3)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x6)) → step_x_f(rev_l, foldr#3(x6))
main(Nil) → Nil
main(Cons(x9)) → step_x_f#1(rev_l, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_rev_l2_0 :: rev_l
hole_step_x_f:fleft_op_e_xs_13_0 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_15_0 :: Nat → step_x_f:fleft_op_e_xs_1

Lemmas:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(+(1, n7_0), b)), rt ∈ Ω(1 + n7₀)
foldr#3(gen_Cons:Nil4_0(n499_0)) → gen_step_x_f:fleft_op_e_xs_15_0(n499_0), rt ∈ Ω(1 + n499₀)

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(gen_Cons:Nil4_0(x))
gen_step_x_f:fleft_op_e_xs_15_0(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_15_0(+(x, 1)) ⇔ step_x_f(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(x))

No more defined symbols left to analyse.

(18) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(+(1, n7_0), b)), rt ∈ Ω(1 + n7₀)

(19) BOUNDS(n^1, INF)

(20) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8) → Cons(x8)
step_x_f#1(rev_l, step_x_f(x2, x4), x1) → step_x_f#1(x2, x4, rev_l#2(x1))
step_x_f#1(rev_l, fleft_op_e_xs_1, x3) → rev_l#2(x3)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x6)) → step_x_f(rev_l, foldr#3(x6))
main(Nil) → Nil
main(Cons(x9)) → step_x_f#1(rev_l, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_0 :: Cons:Nil
hole_rev_l2_0 :: rev_l
hole_step_x_f:fleft_op_e_xs_13_0 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_15_0 :: Nat → step_x_f:fleft_op_e_xs_1

Lemmas:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(+(1, n7_0), b)), rt ∈ Ω(1 + n7₀)

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(gen_Cons:Nil4_0(x))
gen_step_x_f:fleft_op_e_xs_15_0(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_15_0(+(x, 1)) ⇔ step_x_f(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(x))

No more defined symbols left to analyse.

(21) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
step_x_f#1(rev_l, gen_step_x_f:fleft_op_e_xs_15_0(n7_0), gen_Cons:Nil4_0(b)) → gen_Cons:Nil4_0(+(+(1, n7_0), b)), rt ∈ Ω(1 + n7₀)

(22) BOUNDS(n^1, INF)